COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00006 00003	.<<solutions>>
C00012 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.turn on "→"
CS206∂(30)FINAL EXAMINATION→FALL 1976

	This examination is open book and notes.
Write LISP functions as follows except where something else is
requested.  Either notation may be used.

1. %2noccurl[x,u]%1 is the number of occurrences of the S-expression
⊗x in the list ⊗u (at the top level).

Example: %2noccurl[%1(A) , ((A) B ((A)) (A) A)] = 2.

2. %2noccurs[x,y]%1 is the number of occurrences of the S-expression
⊗x in the S-expression ⊗y (anywhere).

Example: %2noccurs%1[(A) , ((A) B ((A)) (A) A)] = 4.

3. %2samefringe[x,y]%1 is true if ⊗x and ⊗y have the same atoms
in the same order.  Thus

	%2samefringe[%1((A.B).C) , (A.(B.C))].

Write ⊗samefringe without flattening the lists ⊗x and ⊗y. 

4. We define

	%2prina[e,l] ← qif qat e qthen e . l qelse %1LP . %2prina[qa e,
%1DOT%2 . prina[qd e, %1RP%2 . l]]%1.

so that

	%2prina%1[(PLUS (TIMES A B) C),NIL] = (LP PLUS DOT LP LP TIMES
DOT LP A DOT LP B DOT NIL RP RP RP DOT LP C DOT NIL RP RP RP),

i.e. ⊗prina "prints" an S-expression in "dot" notation.

On the other hand

	%2prinb%1[(PLUS (TIMES A B) C)] = (LP PLUS LP TIMES A B RP C RP),

i.e. ⊗prinb "prints" an S-expression in "list" notation.

Hint: The second argument in each case is a list of the items to follow
the "printout" of the first expression.  It is there to make the
recursion work.

5. We have 

	%2drop u ← qif qn u qthen qNIL qelse <qa u> . drop qd u%1.

Prove that for all lists ⊗u and ⊗v 

	%2drop[u * v] = drop u * drop v%1.

6. A list structure is called compact if EQUAL subexpressions
are represented by the same list structure.  Thus
.skip 4
is a compact version of
.skip 4
and both represent the S-expression ((A) A).

	%2compact x%1 is a compact list structure EQUAL to ⊗x. 

How does the running time of your ⊗compact depend on the size of
⊗x?  How fast a version do you think can be written?  How
would it work?
.<<solutions>>
.next page
.turn off "["
.turn off "{"
.TURN ON "→"
.turn on "α"
CS206∂(27)SOLUTIONS TO FINAL→FALL 1976

1. %2noccurl[x , u] ← qif qn u qthen 0 qelse [qif x = qa u qthen 1 qelse 0]
 + noccurl[x , qd u]%1.

2. %2noccurs[x , y] ← qif x = y qthen 1 qelse qif qat y qthen 0
qelse noccurs[x , qa y] + noccurs[x, qd y]%1.

3. There are many solutions to the %2samefringe%1 problem which has
been proposed as an example requiring co-routines.  Here one of the
simplest:

%2samefringe[x, y] ← x %3eq %2y ∨ [¬%3at %2x ∧
¬%3at %2y ∧ same[gopher x, gopher y]]

%2same[x, y] ← %3a %2x %3eq a %3y ∧
%2samefringe[%3d %2 x, %3d %2y]

%2gopher u ← %3if at a %2u %3then%2 u
%3else%2 gopher %3aa %2u . [%3da %2u . %3d %2u]
%1

%2gopher%1 digs up the first atom in an S-expression, piling
up the %2cdr%1s (with its hind legs) so that the indexing
through the atoms can be continued.
.nofill

4. %2prinb[e, l] ← qif qat e qthen e . l
∂(15)qelse %1LP%2 .
∂(20)[qif qn qd e qthen prinb[qa e, %1RP%2 . l]
∂(25)qelse qif qat qd e qthen prinb[qa e, %1DOT%2 . [qd e . [%1RP%2 . l]]]
∂(25)qelse prinb[qa e, qd prinb[qd e, l]]]%1

.fill
5. Let %2P(u)%1 be the assertion %2drop[u * v] = drop u * drop v%1.  The
induction principle is

	%2P[qnil] ∧ ∀u.[P[qd u] ⊃ P[u]] ⊃ ∀u.P[u]%1,

and putting %2P = λu.[drop[u * v] = drop u * drop v]%1 gives
.nofill

∂(10)%2[drop[qnil * v] = drop qnil * drop v]
∂(15)∧ ∀u.[drop[qd u * v] = drop qd u * drop v ⊃ drop[u * v] = drop u * drop v]

∂(10)⊃ ∀u.[drop[u * v] = drop u * drop v]%1.
.fill
We have 
.nofill

%2drop[qnil * v] ∂(15)= drop v ∂(40)%1by %2∀w.qnil * w = w,

∂(15)= qnil * drop v ∂(40) %1by same fact,

∂(15)= drop qnil * drop v ∂(40)drop qnil = qnil %1comes from def. of %2drop%1,

and the last equation is %2P[qnil]%1.  The induction step is

.skip to column 1
%2drop[u * v]∂(12) = drop[qif qn u qthen v qelse qa u .[q u * v]]→%1by def. %2u * v

∂(12)= qif qn u qthen drop v qelse drop[qa u . [qd u * v]]→%1by distrib. of c.e.%2

∂(12)= qif qn u qthen drop v qelse <qa [qa u . [qd u * v]]> . drop qd [qa u .[qd u * v]]
%1by def. of %2drop%1 and %2∀x y.¬qn[x . y]%1,

∂(12)= qif qn u qthen drop v qelse <qa u> . drop [qd u * v]→by qa and qd rules,%2

∂(12)= qif qn u qthen drop v qelse <qa u> . [drop qd u * drop v]→%1by induction hypothesis%2,

∂(12)= qif qn u qthen qnil * drop v qelse [<qa u> . drop qd u] * drop v
%1by %2∀w.[qnil * w = w]%1 and def. of %2[<qa u> . drop qd u] * drop v,

∂(12)= [qif qn u qthen qnil qelse <qa u> . drop qd u] * drop v→%1distrib. of c.e%2

∂(12)= drop u * drop v%1→%1by def. of %2drop v%1,
.fill
which is the result to be proved.
.nofill

6. %2compact x ← qa compact1[x, qnil]

compact1[x, u] ←∂(16){find[x, u]}[λz. 
∂(20)qif ¬qn z qthen qa z . u
∂(20)qelse qif qat x qthen x . u
∂(20)qelse α{compact1[qa x, u]}[λx1. 
∂(25){compact1[qd x, qd x1]}[λx2. 
∂(30)qif qa x qeq qa x1 ∧ qd x qeq qa x2 qthen x . [x . qd x2]
∂(30)qelse α{qa x1 . qa x2}[λv. v . [v . qd x2]]]]]

find[x, u] ← qif qn u qthen qNIL qelse qif x = qa u qthen u qelse find[x, qd u]
.fill
%1
	The following solution by Roy Harrington seems better than mine,
but I haven't taken time to analyze it:
.nofill

%2compact x ← comp[x, qNIL]

%2comp[x, y] ← ∂(13)qif qat x qthen x
∂(13)qelse {mem[x,y]}[λs.∂(30)qif ¬qn s qthen s
∂(30)qelse {comp[qd x, y]}[λz. comp[qa x, z . y] . z]]

mem[x, y] ← ∂(12)qif x = y qthen y
∂(12)qelse qif qat y qthen qNIL
∂(12)qelse {mem[x, qa y]}[λz. qif qn z qthen mem[x, qd y] qelse z]]